private import csharp
private import semmle.code.csharp.frameworks.system.collections.Generic as GenericCollections
private import semmle.code.csharp.dataflow.internal.DataFlowPrivate
private import semmle.code.csharp.frameworks.system.linq.Expressions
private import CaptureModels::ModelGeneratorCommonInput as ModelGeneratorInput
private import CaptureModels::SummaryModelGeneratorInput as SummaryModelGeneratorInput
private import CaptureModelsPrinting

/**
 * Holds if `t` is a subtype (reflexive/transitive) of `IEnumerable<T>`, where `T` = `tp`.
 */
private predicate genericCollectionType(ValueOrRefType t, TypeParameter tp) {
  exists(ConstructedGeneric t2 |
    t2 = t.getABaseType*() and
    t2.getUnboundDeclaration() instanceof
      GenericCollections::SystemCollectionsGenericIEnumerableTInterface and
    tp = t2.getATypeArgument()
  )
}

/**
 * Holds if `tp` is a type parameter of the immediate type declaring `callable`.
 */
private predicate classTypeParameter(Callable callable, TypeParameter tp) {
  callable.getDeclaringType().(UnboundGeneric).getATypeParameter() = tp
}

/**
 * Holds if `tp` is type parameter of `callable` or the type declaring `callable`.
 */
private predicate localTypeParameter(Callable callable, TypeParameter tp) {
  classTypeParameter(callable, tp) or
  callable.(UnboundGeneric).getATypeParameter() = tp
}

/**
 * Holds if `callable` has a parameter of type `tp`
 * or collection parameterized over type `tp`.
 */
private predicate parameter(Callable callable, string input, TypeParameter tp) {
  exists(Parameter p |
    input = ModelGeneratorInput::parameterApproximateAccess(p) and
    p = callable.getAParameter() and
    (
      // Parameter of type tp
      p.getType() = tp
      or
      // Parameter is a collection of type tp
      genericCollectionType(p.getType(), tp)
    )
  )
}

/**
 * Gets the string representation of a synthetic field corresponding to `tp`.
 */
private string getSyntheticField(TypeParameter tp) {
  result = ".SyntheticField[ArgType" + tp.getIndex() + "]"
}

/**
 * Gets a models as data string representation of, how a value of type `tp`
 * can be read or stored implicitly in relation to `callable`.
 */
private string implicit(Callable callable, TypeParameter tp) {
  classTypeParameter(callable, tp) and
  not callable.(Modifiable).isStatic() and
  exists(string access |
    if genericCollectionType(callable.getDeclaringType(), tp)
    then access = ".Element"
    else access = getSyntheticField(tp)
  |
    result = ModelGeneratorInput::qualifierString() + access
  )
}

/**
 * Holds if `callable` has a delegate parameter `dt` at parameter position `position`.
 */
private predicate delegate(Callable callable, DelegateType dt, int position) {
  exists(Parameter p |
    p = callable.getAParameter() and
    dt = p.getType().(SystemLinqExpressions::DelegateExtType).getDelegateType() and
    position = p.getPosition()
  )
}

/**
 * Gets models as data input/output access relative to the type parameter `tp` in the
 * type `t` in the scope of `callable`.
 *
 * Note: This predicate has to be inlined as `callable` is not related to `return` or `tp`
 * in every disjunction.
 */
bindingset[callable]
private string getAccess(Callable callable, Type return, TypeParameter tp) {
  return = tp and result = ""
  or
  genericCollectionType(return, tp) and result = ".Element"
  or
  not genericCollectionType(return, tp) and
  (
    return.(ConstructedGeneric).getATypeArgument() = tp
    or
    callable.getDeclaringType() = return and return.(UnboundGeneric).getATypeParameter() = tp
  ) and
  result = getSyntheticField(tp)
}

/**
 * Holds if `input` is a models as data string representation of, how a value of type `tp`
 * (or a generic parameterized over `tp`) can be generated by a delegate parameter of `callable`.
 */
private predicate delegateSource(Callable callable, string input, TypeParameter tp) {
  exists(DelegateType dt, int position, Type return, string access |
    delegate(callable, dt, position) and
    return = dt.getReturnType() and
    access = getAccess(callable, return, tp) and
    input = "Argument[" + position + "].ReturnValue" + access
  )
}

/**
 * Holds if `input` is a models as data string representation of, how a
 * value of type `tp` (or a generic parameterized over `tp`)
 * can be provided as input to `callable`.
 * This includes
 * (1) The implicit synthetic field(s) of the declaring type of `callable`.
 * (2) The parameters of `callable`.
 * (3) Any delegate parameters of `callable`.
 */
private predicate input(Callable callable, string input, TypeParameter tp) {
  input = implicit(callable, tp)
  or
  parameter(callable, input, tp)
  or
  delegateSource(callable, input, tp)
}

/**
 * Holds if `callable` returns a value of type `tp` (or a generic parameterized over `tp`) and `output`
 * is a models as data string representation of, how data is routed to the return.
 */
private predicate returns(Callable callable, TypeParameter tp, string output) {
  exists(Type return, string access | return = callable.getReturnType() |
    access = getAccess(callable, return, tp) and
    output = "ReturnValue" + access
  )
}

/**
 * Holds if `callable` has a delegate parameter that accepts a value of type `tp`
 * and `output` is the models as data string representation of, how data is routed to
 * the delegate parameter.
 */
private predicate delegateSink(Callable callable, TypeParameter tp, string output) {
  exists(DelegateType dt, int position, Parameter p |
    delegate(callable, dt, position) and
    p = dt.getAParameter() and
    p.getType() = tp and
    output = "Argument[" + position + "]" + ".Parameter[" + p.getPosition() + "]"
  )
}

/**
 * Holds if `output` is a models as data string representation of, how values of type `tp`
 * (or generics parameterized over `tp`) can be routed.
 * This includes
 * (1) The implicit synthetic field(s) of the declaring type of `callable`.
 * (2) The return of `callable`.
 * (3) Any delegate parameters of `callable`.
 */
private predicate output(Callable callable, TypeParameter tp, string output) {
  output = implicit(callable, tp)
  or
  returns(callable, tp, output)
  or
  delegateSink(callable, tp, output)
}

private module ModelPrintingInput implements ModelPrintingSummarySig {
  class SummaryApi = TypeBasedFlowTargetApi;

  string getProvenance() { result = "tb-generated" }
}

private module Printing = ModelPrintingSummary<ModelPrintingInput>;

/**
 * A class of callables that are relevant generating summaries for based
 * on the Theorems for Free approach.
 */
class TypeBasedFlowTargetApi extends SummaryModelGeneratorInput::SummaryTargetApi {
  /**
   * Gets the string representation of all type based summaries for `this`
   * inspired by the Theorems for Free approach.
   *
   * Examples could be (see C# pseudo code below)
   * (1) `Get` returns a value of type `T`. We assume that the returned
   *     value was fetched from a (synthetic) field.
   * (2) `Set` consumes a value of type `T`. We assume that the value is stored in
   *     a (synthetic) field.
   * (3) `Apply<S>` is assumed to apply the provided function to a value stored in
   *     a (synthetic) field and return the result.
   * (4) `Apply<S1,S2>` is assumed to apply the provided function to provided value
   *     and return the result.
   * ```csharp
   * public class MyGeneric<T> {
   *    public void Set(T x) { ... }
   *    public T Get() { ... }
   *    public S Apply<S>(Func<T, S> f) { ... }
   *    public S2 Apply<S1, S2>(S1 x, Func<S1, S2> f) { ... }
   * }
   * ```
   */
  string getSummaries() {
    exists(TypeParameter tp, string input, string output |
      localTypeParameter(this, tp) and
      input(this, input, tp) and
      output(this, tp, output) and
      input != output
    |
      result = Printing::asLiftedValueModel(this, input, output)
    )
  }
}

/**
 * Returns the Theorems for Free inspired typed based summaries for `api`.
 */
string captureFlow(TypeBasedFlowTargetApi api) { result = api.getSummaries() }
